perm filename FIRST.LEC[W79,JMC] blob sn#419787 filedate 1979-02-20 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	NOTES FOR LECTURE ON PROVING PROPERTIES OF RECURSIVE PROGRAMS
C00003 ENDMK
CāŠ—;
NOTES FOR LECTURE ON PROVING PROPERTIES OF RECURSIVE PROGRAMS


Example programs

	n!

append

91 function

flat

samefringe

takeuchi

corectness of append.  There is a unique function u*v
such that nil*u = u and [x.u]*v = x.[u*v].  This is because

u*v ā† qif qn u qthen v qelse qa u . [qd u * v]

is total.

extensional properties